The following is a list of topics and results of homotopy theory that have been formalized in homotopy type theory.
On homotopy groups of spheres:
Dan’s construction.
is a spectrum, formalized
Cohomology of the n-torus, which could be easily extended to any finite product of spheres.
to do:
cohomology with finite coefficients, all we need is the boring work of defining as an explicit group.
Calculate some more cohomology groups.
Compute the loop space of this construction and use it to define spectra.
On the Freudenthal suspension theorem:
Implies whenever
Peter’s encode/decode-style proof, formalized by Dan, using a clever lemma about maps out of 2 n-connected types. This is the “95%” version, which shows that the relevant map is an equivalence on truncations.
The full “100%” version, formalized by Dan, which shows that the relevant map is -connected.
On homotopy limits:
On the van Kampen theorem:
On covering spaces:
Created on June 9, 2022 at 07:13:54. See the history of this page for a list of all contributions to it.